T:Type, as, bs, cs, ds:T List.
(xcs. (x  bs))
 (xas. (x  ds))
 agree_on_common(T;as;cs)
 agree_on_common(T;bs;ds)
 agree_on_common(T;as @ bs;cs @ ds) 

latex

Definitions	t  T, x:A. B(x), (x  l), A, x. t(x), xL. P(x), agree_on_common(T;as;bs), P  Q, as @ bs, P & Q, P  Q, True, False, P  Q, Prop, {T}, P  Q
Lemmas	cons member, member append, all functionality wrt iff, implies functionality wrt iff, agree on common nil, agree on common cons2, append wf, l all cons, agree on common wf, l all wf, not wf, l member wf